es:ES, i:Id, e':E, P:({e:E| loc(e) = i }Prop).
e@i. Dec(P(e))  loc(e') = i  (e<e'.e is first@ i s.t.  e.P(e)  e<e'.P(e)) 

latex

Definitions	x:A. B(x), Prop, P  Q, x(s), P  Q, P & Q, P  Q, t  T, x. t(x), e<e'.P(e), x:A. B(x), A & B, A, e@i. P(e), P  Q, {T}, e is first@ i s.t.  e.P(e), e<e'. P(e), (e <loc e'), WellFnd{i}(A;x,y.R(x;y)), False, Dec(P)
Lemmas	existse-before wf, es-first-at wf, es-E wf, Id wf, es-loc wf, alle-at wf, decidable wf, event system wf, es-locl wf, es-loc-pred, es-locl-iff, es-locl-wellfnd, es-first-implies, assert wf, es-first wf, decidable existse-before, es-pred wf, existse-before-iff, es-pred-locl